function strval(k){return k.toString();}